\begin{tabbing}
$\forall$$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$).
\\[0ex]normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ l\_all(\=ecl{-}kinds($A$);\+
\\[0ex]Knd;
\\[0ex]$k$.((($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$)) $\in$ Id)) $\wedge$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$)))
\\[0ex])
\-\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=ecl{-}machine1\=\{ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$);
\-\\[0ex]${\it es}$.(es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=(subtype\_rel(\=es{-}vartype(${\it es}$; $i$; mkid\{ecl:ut2\});\+\+
\\[0ex]ecl{-}trans{-}type(ecl{-}trans($A$)))
\-\\[0ex]c$\wedge$ \=($\forall$$n$:$\mathbb{N}$. \+
\\[0ex]alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(($\uparrow$es{-}bact\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$; $A$; ${\it es}$; $n$; es{-}init(${\it es}$;$e$); $e$))
\-\\[0ex]$\Leftarrow\!\Rightarrow$ \=((es{-}kind(${\it es}$; $e$) $\in$ ecl{-}trans{-}ks(ecl{-}trans($A$)))\+
\\[0ex]c$\wedge$ ($\uparrow$(\=ecl{-}trans{-}a(ecl{-}trans($A$))\+
\\[0ex]($n$
\\[0ex],es{-}kind(${\it es}$; $e$)
\\[0ex],es{-}state{-}when(${\it es}$; $e$)
\\[0ex],es{-}val(${\it es}$; $e$)
\\[0ex],es{-}when(${\it es}$; mkid\{ecl:ut2\}; $e$)))))))))))
\-\-\-\-\-\-\-
\end{tabbing}